eclseq($a$;$b$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inl($\langle$$a$$,\,$$b$$\rangle$))